\relax 
\@writefile{toc}{\contentsline {section}{\numberline {1}\hskip -1em.\nobreakspace  {}Introduction}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {2}\hskip -1em.\nobreakspace  {}Contract Expressivity}{1}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces An Increment specification in C{\normalfont  \#}}}{1}}
\newlabel{fig:csharp}{{1}{1}}
\citation{Liskov-Wing94}
\@writefile{toc}{\contentsline {section}{\numberline {3}\hskip -1em.\nobreakspace  {}Runtime Contract Checking}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {4}\hskip -1em.\nobreakspace  {}Static Checking}{2}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces An Increment specification in Visual Basic}}{2}}
\newlabel{fig:vb}{{3}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Screenshots}{2}}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Example of Runtime Contract Failure}}{2}}
\newlabel{fig:foxtrot}{{4}{2}}
\bibstyle{latex8}
\bibdata{bib}
\bibcite{godefroid05:dart}{1}
\bibcite{Liskov-Wing94}{2}
\bibcite{nunit}{3}
\bibcite{mstest}{4}
\bibcite{pex}{5}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces The Code Contact User Interface}}{3}}
\newlabel{fig:contractui}{{2}{3}}
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces Example of Static Checker Output}}{4}}
\newlabel{fig:clousot}{{5}{4}}
